Abstract: Phishing is a form of electronic identity theft in which social engineering and website spoofing techniques are employed to trick a user into revealing confidential information. In this research, a previously proposed behaviour based anti-phishing approach model is verified using model checking. SPIN model checker is used to check the absence of deadlocks as well as reachable states. SPIN illustrates that there is no error since it does not report “invalid end state” as there is no deadlock in the model. There is also no error and unexecuted codes since as all processes have “zero” unreached states and the trail number equals to “zero”. Formal verification using SPIN is applied to help checking whether the model is feasible and applicable. This helps deploying the approach model in the real world in order to enhance phishing countermeasures within LANs.

Keywords: